Nuprl Lemma : preserved_by2_wf 4,23

T:Type, P:(TProp), R:(TTTProp). (ternary) R preserves P   Prop 
latex


Definitions(ternary) R preserves P , x:AB(x), P  Q, Prop, t  T

origin